1) Declaration section

In this section, we declare the parameter used in protocol description. They include:

Agents

It starts with the keyword #Agents followed by the list of agents names used in the protocols.

Servers

It starts with the keyword #Servers followed by the list of servers names used in the protocols.

Nonces

It starts with the keyword #Nonces followed by the list of nonces used in the protocols.

Public keys

It starts with the keyword #Public_keys followed by the list of public keys used in the protocols.

Server keys

It starts with the keyword #Server_keys followed by the list of server keys used in the protocols.

Signature keys

It starts with the keyword #Signature_keys followed by the list of signature keys used in the protocols.

Inverse keys

It starts with the keyword #Inverse_keys followed by the list of inverse keys used in the protocols.

Constants

It starts with the keyword #Constants followed by the list of constant values used in the protocols.

Functions

It starts with the keyword #Functions followed by the list of functions name used in the protocols.

2) Initial knowledge section

In this section, we declare the initial knowledge of agents participating in the protocol. It consists of declaration lines, each line has the syntax:

agents knows {list of knowledge};

3) Protocol description section

This section describes the communication between participants. It consists of description lines, each line has the syntax:

participant1 -> participant2 : message

4) Actual system section

This section declares the actual participants involving in the protocol. It consists:

Initiator

Declare the actual name of initiators involved in the protocol. It starts with the keyword #Initiator followed by the list of participants names.

Responder

Declare the actual name of responders involved in the protocol. It starts with the keyword #Responder followed by the list of participants names.

Server

Declare the actual name of servers involved in the protocol. It starts with the keyword #Server followed by the list of participants names.

5) Intruder section

This section declares the information of the intruder. It consists:

Intruder name

Declare the name of intruder participating in the protocol. It starts with the keyword #Intruder: followed by the intruder name.

Intruder knowledge

Declare the initial knowledge of the intruder. It starts with the keyword #Intruder_knowledge followed by the list of knowledge.

Intruder_ability

Declare the ability of the intruder. The ability includes: Transmit, Deflect, Inject, Eavesdrop and Jam It starts with the keyword #Intruder_ability followed by the list of ability.